Step of Proof: do-apply-mu' 11,40
Inference at * 
Iof proof for Lemma do-apply-mu':


  A:Type, P:(A), d:(x:A. Dec(n:. ((P(x,n))))), x:A.
  (can-apply(mu'(P);x))
   {((P(x,do-apply(mu'(P);x)))) & (i:{0..do-apply(mu'(P);x)}. ((P(x,i))))} 
latex
 by (Auto) 
CollapseTHEN ((MoveToConcl (-1)) 
CollapseTHEN ((RepUR ``mu\' can-apply do-apply
C`` ( 0)) 
CollapseTHEN ((Subst' TERMOF{p-mu-decider:ObjectId, 1:l, 1:l}
CollapseTHEN ((Subst' TERMOF{p-mu-decider~
CollapseTHEN ((Subst' TERMOF{p-mu-deciderTERMOF{p-mu-decider:ObjectId, 1:l, i:l} ( 0)) 
THENL [(
TRW (SubC (ComputeToC []) ) 0) 
CollapseTHEN (Trivial) ; Id]))) 
latex

C1: 

C1: 1. A : Type
C1: 2. P : A
C1: 3. d : x:A. Dec(n:. ((P(x,n))))
C1: 4. x : A
C1:   (isl((TERMOF{p-mu-decider:ObjectId, 1:l, i:l}(A,P,d,x)).1))
C1:    {((P(x,outl((TERMOF{p-mu-decider:ObjectId, 1:l, i:l}(A,P,d,x)).1))))
C1:    & (i:{0..outl((TERMOF{p-mu-decider:ObjectId, 1:l, i:l}(A,P,d,x)).1)}. ((P(x,i))))}
C.

Definitionss ~ t, p-mu-decider, A, False, {T}, P & Q, {i..j}, suptype(S; T), {x:A| B(x)} , left + right, S  T, Top, x:A.B(x), Void, Dec(P), x:A. B(x), x:A  B(x), x:A. B(x), f(a), , , t  T, Type, P  Q, x:AB(x), can-apply(f;x), mu'(P), do-apply(f;x), b
Lemmascan-apply wf, mu' wf, top wf, decidable wf, assert wf, nat wf, bool wf

origin